↳ Prolog
↳ PrologToPiTRSProof
slowsort_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, .(Y, [])), .(U, .(V, []))) → U5_ga(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aga(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aga(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ga(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ga(X, Y, U, V, perm_in_ga(Z, V))
U6_ga(X, Y, U, V, perm_out_ga(Z, V)) → perm_out_ga(.(X, .(Y, [])), .(U, .(V, [])))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ga(X, Y, sorted_out_g(Y)) → slowsort_out_ga(X, Y)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
slowsort_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, .(Y, [])), .(U, .(V, []))) → U5_ga(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aga(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aga(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ga(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ga(X, Y, U, V, perm_in_ga(Z, V))
U6_ga(X, Y, U, V, perm_out_ga(Z, V)) → perm_out_ga(.(X, .(Y, [])), .(U, .(V, [])))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ga(X, Y, sorted_out_g(Y)) → slowsort_out_ga(X, Y)
SLOWSORT_IN_GA(X, Y) → U1_GA(X, Y, perm_in_ga(X, Y))
SLOWSORT_IN_GA(X, Y) → PERM_IN_GA(X, Y)
PERM_IN_GA(.(X, .(Y, [])), .(U, .(V, []))) → U5_GA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
PERM_IN_GA(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_AGA(U, .(X, Y), Z)
DELETE_IN_AGA(X, .(Y, Z), W) → U7_AGA(X, Y, Z, W, delete_in_aga(X, Z, W))
DELETE_IN_AGA(X, .(Y, Z), W) → DELETE_IN_AGA(X, Z, W)
U5_GA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_GA(X, Y, U, V, perm_in_ga(Z, V))
U5_GA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_GA(Z, V)
U1_GA(X, Y, perm_out_ga(X, Y)) → U2_GA(X, Y, sorted_in_g(Y))
U1_GA(X, Y, perm_out_ga(X, Y)) → SORTED_IN_G(Y)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
SORTED_IN_G(.(X, .(Y, Z))) → LE_IN_GG(X, Y)
LE_IN_GG(s(X), s(Y)) → U8_GG(X, Y, le_in_gg(X, Y))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
U3_G(X, Y, Z, le_out_gg(X, Y)) → U4_G(X, Y, Z, sorted_in_g(.(Y, Z)))
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
slowsort_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, .(Y, [])), .(U, .(V, []))) → U5_ga(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aga(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aga(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ga(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ga(X, Y, U, V, perm_in_ga(Z, V))
U6_ga(X, Y, U, V, perm_out_ga(Z, V)) → perm_out_ga(.(X, .(Y, [])), .(U, .(V, [])))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ga(X, Y, sorted_out_g(Y)) → slowsort_out_ga(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
SLOWSORT_IN_GA(X, Y) → U1_GA(X, Y, perm_in_ga(X, Y))
SLOWSORT_IN_GA(X, Y) → PERM_IN_GA(X, Y)
PERM_IN_GA(.(X, .(Y, [])), .(U, .(V, []))) → U5_GA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
PERM_IN_GA(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_AGA(U, .(X, Y), Z)
DELETE_IN_AGA(X, .(Y, Z), W) → U7_AGA(X, Y, Z, W, delete_in_aga(X, Z, W))
DELETE_IN_AGA(X, .(Y, Z), W) → DELETE_IN_AGA(X, Z, W)
U5_GA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_GA(X, Y, U, V, perm_in_ga(Z, V))
U5_GA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_GA(Z, V)
U1_GA(X, Y, perm_out_ga(X, Y)) → U2_GA(X, Y, sorted_in_g(Y))
U1_GA(X, Y, perm_out_ga(X, Y)) → SORTED_IN_G(Y)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
SORTED_IN_G(.(X, .(Y, Z))) → LE_IN_GG(X, Y)
LE_IN_GG(s(X), s(Y)) → U8_GG(X, Y, le_in_gg(X, Y))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
U3_G(X, Y, Z, le_out_gg(X, Y)) → U4_G(X, Y, Z, sorted_in_g(.(Y, Z)))
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
slowsort_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, .(Y, [])), .(U, .(V, []))) → U5_ga(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aga(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aga(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ga(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ga(X, Y, U, V, perm_in_ga(Z, V))
U6_ga(X, Y, U, V, perm_out_ga(Z, V)) → perm_out_ga(.(X, .(Y, [])), .(U, .(V, [])))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ga(X, Y, sorted_out_g(Y)) → slowsort_out_ga(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
slowsort_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, .(Y, [])), .(U, .(V, []))) → U5_ga(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aga(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aga(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ga(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ga(X, Y, U, V, perm_in_ga(Z, V))
U6_ga(X, Y, U, V, perm_out_ga(Z, V)) → perm_out_ga(.(X, .(Y, [])), .(U, .(V, [])))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ga(X, Y, sorted_out_g(Y)) → slowsort_out_ga(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
slowsort_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, .(Y, [])), .(U, .(V, []))) → U5_ga(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aga(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aga(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ga(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ga(X, Y, U, V, perm_in_ga(Z, V))
U6_ga(X, Y, U, V, perm_out_ga(Z, V)) → perm_out_ga(.(X, .(Y, [])), .(U, .(V, [])))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ga(X, Y, sorted_out_g(Y)) → slowsort_out_ga(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
U3_G(X, Y, Z, le_out_gg(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ PiDP
↳ PiDP
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(Y, Z, le_in_gg(X, Y))
U3_G(Y, Z, le_out_gg) → SORTED_IN_G(.(Y, Z))
le_in_gg(s(X), s(Y)) → U8_gg(le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg
le_in_gg(0, 0) → le_out_gg
U8_gg(le_out_gg) → le_out_gg
le_in_gg(x0, x1)
U8_gg(x0)
The following rules are removed from R:
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(Y, Z, le_in_gg(X, Y))
U3_G(Y, Z, le_out_gg) → SORTED_IN_G(.(Y, Z))
Used ordering: POLO with Polynomial interpretation [25]:
le_in_gg(s(X), s(Y)) → U8_gg(le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg
le_in_gg(0, 0) → le_out_gg
U8_gg(le_out_gg) → le_out_gg
POL(.(x1, x2)) = 2 + 2·x1 + 2·x2
POL(0) = 1
POL(SORTED_IN_G(x1)) = 1 + x1
POL(U3_G(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3
POL(U8_gg(x1)) = 2 + x1
POL(le_in_gg(x1, x2)) = x1 + x2
POL(le_out_gg) = 2
POL(s(x1)) = 1 + 2·x1
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ PiDP
↳ PiDP
le_in_gg(x0, x1)
U8_gg(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
DELETE_IN_AGA(X, .(Y, Z), W) → DELETE_IN_AGA(X, Z, W)
slowsort_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, .(Y, [])), .(U, .(V, []))) → U5_ga(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aga(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aga(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ga(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ga(X, Y, U, V, perm_in_ga(Z, V))
U6_ga(X, Y, U, V, perm_out_ga(Z, V)) → perm_out_ga(.(X, .(Y, [])), .(U, .(V, [])))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ga(X, Y, sorted_out_g(Y)) → slowsort_out_ga(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
DELETE_IN_AGA(X, .(Y, Z), W) → DELETE_IN_AGA(X, Z, W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
DELETE_IN_AGA(.(Y, Z)) → DELETE_IN_AGA(Z)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
PERM_IN_GA(.(X, .(Y, [])), .(U, .(V, []))) → U5_GA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_GA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_GA(Z, V)
slowsort_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, .(Y, [])), .(U, .(V, []))) → U5_ga(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aga(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aga(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ga(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ga(X, Y, U, V, perm_in_ga(Z, V))
U6_ga(X, Y, U, V, perm_out_ga(Z, V)) → perm_out_ga(.(X, .(Y, [])), .(U, .(V, [])))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(X)) → le_out_gg(0, s(X))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U3_g(X, Y, Z, le_out_gg(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ga(X, Y, sorted_out_g(Y)) → slowsort_out_ga(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
PERM_IN_GA(.(X, .(Y, [])), .(U, .(V, []))) → U5_GA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_GA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_GA(Z, V)
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aga(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aga(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
PERM_IN_GA(.(X, .(Y, []))) → U5_GA(delete_in_aga(.(X, Y)))
U5_GA(delete_out_aga(U, Z)) → PERM_IN_GA(Z)
delete_in_aga(.(X, Y)) → delete_out_aga(X, Y)
delete_in_aga(.(Y, Z)) → U7_aga(delete_in_aga(Z))
U7_aga(delete_out_aga(X, W)) → delete_out_aga(X, W)
delete_in_aga(x0)
U7_aga(x0)
No rules are removed from R.
PERM_IN_GA(.(X, .(Y, []))) → U5_GA(delete_in_aga(.(X, Y)))
POL(.(x1, x2)) = x1 + 2·x2
POL(PERM_IN_GA(x1)) = 1 + x1
POL(U5_GA(x1)) = 1 + x1
POL(U7_aga(x1)) = 2·x1
POL([]) = 0
POL(delete_in_aga(x1)) = x1
POL(delete_out_aga(x1, x2)) = x1 + 2·x2
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ DependencyGraphProof
U5_GA(delete_out_aga(U, Z)) → PERM_IN_GA(Z)
delete_in_aga(.(X, Y)) → delete_out_aga(X, Y)
delete_in_aga(.(Y, Z)) → U7_aga(delete_in_aga(Z))
U7_aga(delete_out_aga(X, W)) → delete_out_aga(X, W)
delete_in_aga(x0)
U7_aga(x0)